Nuprl Lemma : seq-count_wf
11,40
postcript
pdf
T
:Type,
eq
:(
T
T
),
f
:(
T
),
x
:
T
,
j
:
. #{i<
j
|
f
i
eq
x
}
{0..(
j
+1)
}
latex
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
.
B
(
x
)
,
#$n
,
{
i
..
j
}
,
A
B
,
S
T
,
P
&
Q
,
i
j
<
k
,
suptype(
S
;
T
)
,
f
(
a
)
,
f
o
g
,
size(
k
;
f
)
,
#{i<
j
|
f
i
eq
x
}
Lemmas
bool-size
wf
,
compose
wf
,
le
wf
,
int
seg
wf
,
nat
wf
,
bool
wf
origin
T:Type, eq:(T
T
), f:(
T), x:T, j:. #{i<j|f i eq x} 
{0..(j+1)
} T:Type, eq:(TT), f:(T), x:T, j:. #{i<j|f i eq x} {0..(j+1)} TB(x)x:A. B(x)}
B
T j < ksize(k;f)